
Functional Programming and HOL Light

* Intro

** Formal proof

*** Kepler

*** Logic

Axioms, inference rules

*** (M)eta-(L)ogic


* Functional Programming

** Functions

** Types

** Modules

Data structures can only be manipulated by signature

* HOL Light

** HOL Light = Logic (HOL) + meta-logic (Ocaml)



* Course Overview

** Components

*** Lectures

*** Labs

Learn by doing.  Lots of exercises.

** Goals, expectations
